Nuprl Lemma : scheme-plus_wf
11,40
postcript
pdf
A
,
B
:RealizerScheme{i:l}(). scheme-plus(
A
;
B
)
RealizerScheme{i:l}()
latex
Definitions
x
:
A
.
B
(
x
)
,
Id
,
A
B
,
{
x
:
A
|
B
(
x
)}
,
,
P
Q
,
Namer(
n
;
Id_list
)
,
False
,
A
,
A
B
,
,
t
T
,
x
:
A
B
(
x
)
,
namer-shift(
n
;
namer
)
,
f
(
a
)
,
left
right
,
x
.
A
(
x
)
,
Realizer
,
<
a
,
b
>
,
type
List
,
x
:
A
B
(
x
)
,
let
x
,
y
,
z
=
a
in
t
(
x
;
y
;
z
)
,
scheme-plus(
A
;
B
)
,
RealizerScheme{i:l}()
Lemmas
Rplus
wf
,
namer-shift
wf
,
l
contains
append
,
Namer-subtype
,
l
contains
append2
origin
A, B:RealizerScheme{i:l}(). scheme-plus(A;B) 
RealizerScheme{i:l}() A, B:RealizerScheme{i:l}(). scheme-plus(A;B) RealizerScheme{i:l}() x:A. B(x)
B
Q
A
B
T
B(x)
right
x.A(x)
B(x)